conjunctive normal form

Definition (CNF)

Boolean formula over variables $u_1,...,u_n$ is in CNF form if it is an AND of OR's in variables or their negation, or more generally,

where each variable $v_{i_j}$ is either a variable $u_k$ or its negation $\bar{u}_k$. The terms $v_{i_j}$ are called literals of the formula, and terms $\lor_j v_{i_j}$ are called its clauses.

Definition ($k$CNF)

A $k$CNF is a CNF formula in which all clauses contain at most $k$ literals.

See also

• compare to implicative normal form for clauses, where e.g. $a \lor b$ is equivalent to $\lnot a \Rightarrow b \land \lnot b \Rightarrow a$

References

1. S. Arora, B. Barak. Computational Complexity: A Modern Approach, Cambridge University Press, 2009, pp. 44-45.